Code

Simplify known bits#335

Code

Open

morriisw wants to merge 18 commits intomainUQ-PAC/BASIL:mainfrom simplify-known-bitsUQ-PAC/BASIL:simplify-known-bitsCopy head branch name to clipboard

Commits

Commits on Mar 13, 2025

• Initial untested implementation of known bit simplification using trits.

  

  MorrisWang9

  authored and

  ailrst

  committed
  b3a1fff

  Copy full SHA for b3a1fff

• Fix bitwise operation logic.

  

  morriisw

  authored and

  ailrst

  committed
  0f17fd7

  Copy full SHA for 0f17fd7

• Rename file and replace Trit and TritVector classes with TNum class for efficiency and logic simplification. Logic for bitwise operations between TNums remains the same but join method under TNumDo…

  Show description for 8fc40be
  

  morriisw

  authored and

  ailrst

  committed
  8fc40be

  Copy full SHA for 8fc40be

• Simplify transfer method by moving expression matching functionality into a separate method called evaluateExprToTNum to allow for recursive matching and evaluation. Create new method called evalua…

  Show description for 629cca6
  

  morriisw

  authored and

  ailrst

  committed
  629cca6

  Copy full SHA for 629cca6

• Add TNum class methods to handle all supported binary and unary operators. Add evaluateUnOp method under TNumDomain class to handle evaluation of unary operations.

  

  morriisw

  authored and

  ailrst

  committed
  d683d10

  Copy full SHA for d683d10

• Change join method under TNumDomain class to use bitwise OR operation to merge TNum values of variables that appear in both maps.

  

  morriisw

  authored and

  ailrst

  committed
  f0023fa

  Copy full SHA for f0023fa

• Change the logic of all TNum shift operations and fix iv case in the toTNum method under TNumDomain class.

  

  morriisw

  authored and

  ailrst

  committed
  7e45433

  Copy full SHA for 7e45433

• Extend TNum trait and add TNumValue and TNumBool classes to differentiate between bitvector and boolean types. Change bitwise comparison method TCOMP to return a bitvector equivalent TNumValue inst…

  Show description for 00fcfa1
  

  morriisw

  authored and

  ailrst

  committed
  00fcfa1

  Copy full SHA for 00fcfa1

• Add functionality to handle boolean binary and unary operations and translation of literals.

  

  morriisw

  authored and

  ailrst

  committed
  e2b0dea

  Copy full SHA for e2b0dea

• Edit transfer and join methods under TNumDomain class to account for both TNumValue and TNumBool instances.

  

  morriisw

  authored and

  ailrst

  committed
  3ae04cf

  Copy full SHA for 3ae04cf

• add pprinter

  ailrst

  committed
  b3a384a

  Copy full SHA for b3a384a

• fixup printing

  ailrst

  committed
  19b0d57

  Copy full SHA for 19b0d57

• autoformat

  ailrst

  committed
  6c47e15

  Copy full SHA for 6c47e15

• Add Z3 test script that verifies the known bits simplification logic.

  

  morriisw

  authored and

  ailrst

  committed
  775907f

  Copy full SHA for 775907f

• Add explanation of known bits analysis to simplification-solvers.md file.

  

  morriisw

  authored and

  ailrst

  committed
  5449490

  Copy full SHA for 5449490

• Change simplification logic for two's complement negation and fix applyTransform method to generate IL.

  

  morriisw

  authored and

  ailrst

  committed
  74b7cba

  Copy full SHA for 74b7cba

• explicit width

  ailrst

  committed
  f5e635f

  Copy full SHA for f5e635f

• format

  ailrst

  committed
  57fa589

  Copy full SHA for 57fa589