Code

Prototype SMT backend#273

Code

Merged

tnelson merged 167 commits intodevtnelson/Forge:devfrom feat_smttnelson/Forge:feat_smtCopy head branch name to clipboardNov 20, 2024

+10,163-983

Commits

Commits on Jun 18, 2024

• add: working on contract for collector

  tnelson

  committed
  f5958cf

  Copy full SHA for f5958cf

• add: template w/ Karim

  tnelson

  committed
  88127d4

  Copy full SHA for 88127d4

Commits on Jun 19, 2024

• add: Easy way to find Java Temp folder

  tnelson

  committed
  9d1fcc2

  Copy full SHA for 9d1fcc2

Commits on Jun 20, 2024

• change: send-to-kodkod -> send-to-solver

  tnelson

  committed
  ec18c92

  Copy full SHA for ec18c92

• change: factor out pardinus backend

  tnelson

  committed
  1f8de89

  Copy full SHA for 1f8de89

• Merge branch 'dev' into feat_smt

  tnelson

  committed
  e38ad72

  Copy full SHA for e38ad72

• remove: experiment skeleton

  tnelson

  committed
  5e6ed36

  Copy full SHA for 5e6ed36

• Converted to format strings

  k-mouline

  committed
  d2ecaa0

  Copy full SHA for d2ecaa0

• fix: ->

  tnelson

  committed
  7fe890e

  Copy full SHA for 7fe890e

Commits on Jun 21, 2024

• first changes to parsing

  k-mouline

  committed
  b82a887

  Copy full SHA for b82a887

• add: join builder, no preservation of loc

  tnelson

  committed
  19da701

  Copy full SHA for 19da701

• preserve syntax loc

  tnelson

  committed
  dfc9dbc

  Copy full SHA for dfc9dbc

Commits on Jun 24, 2024

• updated interpret calls

  k-mouline

  committed
  03569ec

  Copy full SHA for 03569ec

• examples added

  k-mouline

  committed
  8ec583b

  Copy full SHA for 8ec583b

• pair with Karim, demo of match

  tnelson

  committed
  55e3c5a

  Copy full SHA for 55e3c5a

• identity parsing

  k-mouline

  committed
  c3aed57

  Copy full SHA for c3aed57

• NNF parser

  k-mouline

  committed
  47ae4cf

  Copy full SHA for 47ae4cf

Commits on Jun 25, 2024

• Draft of testing; needs to be validated

  bisheshank

  committed
  87ea87f

  Copy full SHA for 87ea87f

• Substitutor push

  k-mouline

  committed
  68e42ad

  Copy full SHA for 68e42ad

• updated testing; needs review

  bisheshank

  committed
  f61ba63

  Copy full SHA for f61ba63

Commits on Jun 26, 2024

• updating substitutor

  k-mouline

  committed
  17dd94c

  Copy full SHA for 17dd94c

• add: programming together in NNF/NNF testing, macros

  tnelson

  committed
  7d83d9c

  Copy full SHA for 7d83d9c

• quantifiers and decls fixed

  k-mouline

  committed
  5062063

  Copy full SHA for 5062063

• nnf testing updated; need to fix sig-rel contract vio

  bisheshank

  committed
  bf430e4

  Copy full SHA for bf430e4

• small sub tests and nnf conversion modified

  k-mouline

  committed
  d4e8a69

  Copy full SHA for d4e8a69

• verbosity added and sub tests

  k-mouline

  committed
  2c9de2e

  Copy full SHA for 2c9de2e

• nnf-testing suite rewritten

  bisheshank

  committed
  23f820e

  Copy full SHA for 23f820e

• nff-test updated with comparision tests

  bisheshank

  committed
  8d69be9

  Copy full SHA for 8d69be9

Commits on Jun 27, 2024

• refactor: one-sided integration prototype for cvc5

  tnelson

  committed
  44d0280

  Copy full SHA for 44d0280

• skolemization first implementation

  k-mouline

  committed
  f1e5100

  Copy full SHA for f1e5100

• bounds propagate up

  k-mouline

  committed
  ff7e392

  Copy full SHA for ff7e392

Commits on Jun 28, 2024

• add: additional refactoring around SMTlib backend

  tnelson

  committed
  7162ae1

  Copy full SHA for 7162ae1

• minor: print out raw cvc5 response in sat case

  tnelson

  committed
  01dd402

  Copy full SHA for 01dd402

• working: basic parsing of SMTlib SAT response

  tnelson

  committed
  2c8f5c6

  Copy full SHA for 2c8f5c6

• add: own-grandpa, sterling proof of concept

  tnelson

  committed
  eb4c77f

  Copy full SHA for eb4c77f

• integer reconciliation

  k-mouline

  committed
  33f32d1

  Copy full SHA for 33f32d1

• first attempt at converting to smtlib

  k-mouline

  committed
  a912f9a

  Copy full SHA for a912f9a

Commits on Jun 29, 2024

• add: working on integration. NNF and int-conversion in pipeline

  tnelson

  committed
  649d3d6

  Copy full SHA for 649d3d6

• partial conversion, need to stop soon

  tnelson

  committed
  abfa8ed

  Copy full SHA for abfa8ed

• more adjustments to skolem

  tnelson

  committed
  e85656b

  Copy full SHA for e85656b

• add: more fixes, see initialed comments in skolem

  tnelson

  committed
  0c30972

  Copy full SHA for 0c30972

• add: final pipeline step

  tnelson

  committed
  c4c8fd1

  Copy full SHA for c4c8fd1

• working through skolem, starting SMT conversion add

  tnelson

  committed
  658ce7a

  Copy full SHA for 658ce7a

• rough mapping into cvc5, not done yet'

  tnelson

  committed
  45b3297

  Copy full SHA for 45b3297

• working on SMT conversion

  tnelson

  committed
  e26fd69

  Copy full SHA for e26fd69

• fix: skolemize _inner_ formula as well. also fix var call order

  tnelson

  committed
  59ebf96

  Copy full SHA for 59ebf96

• fix: quantifier IDs, more robust cmd line args

  tnelson

  committed
  c709c44

  Copy full SHA for c709c44

• fix: use XSort in quantifier domains

  tnelson

  committed
  7ff052a

  Copy full SHA for 7ff052a

• intermediate checkpoint: multi-run is combining results

  tnelson

  committed
  1805e3c

  Copy full SHA for 1805e3c

• fix: singleton tuple processing. note failing test, skolem issue

  tnelson

  committed
  a4c7d5e

  Copy full SHA for a4c7d5e

Commits on Jun 30, 2024

• fix: skolem depth 0 only; cleanup

  tnelson

  committed
  83697e4

  Copy full SHA for 83697e4

• misc fixes, 3-ary relations

  tnelson

  committed
  33c32fa

  Copy full SHA for 33c32fa

Commits on Jul 1, 2024

• add test

  tnelson

  committed
  171e249

  Copy full SHA for 171e249

• add: print stderr from cvc5 in another location

  tnelson

  committed
  9a1d174

  Copy full SHA for 9a1d174

Commits on Jul 2, 2024

• add: basic collector draft, working on smoke tests

  tnelson

  committed
  52514ab

  Copy full SHA for 52514ab

• update: collector

  tnelson

  committed
  3464314

  Copy full SHA for 3464314

• fix: ordering in collector, add tesT

  tnelson

  committed
  810c352

  Copy full SHA for 810c352

• Small edits to skolemization

  k-mouline

  committed
  ef54bb2

  Copy full SHA for ef54bb2

Commits on Jul 3, 2024

• atom test added

  k-mouline

  committed
  d412ba1

  Copy full SHA for d412ba1

• several changes, mostly multiplicity

  k-mouline

  committed
  ea59bec

  Copy full SHA for ea59bec

• saving intermediate work

  tnelson

  committed
  6218d18

  Copy full SHA for 6218d18

• adding tests

  tnelson

  committed
  504ea94

  Copy full SHA for 504ea94

• paren fix and beginning some work on ints

  k-mouline

  committed
  c46abe5

  Copy full SHA for c46abe5

• disable int literal checking for smtlibtor

  tnelson

  committed
  0396f60

  Copy full SHA for 0396f60

• decl domains are expressions

  tnelson

  committed
  0ab2f30

  Copy full SHA for 0ab2f30

• add: fix errors with skolem, contract

  tnelson

  committed
  5b8a834

  Copy full SHA for 5b8a834

• working; will convert join to application on merge

  tnelson

  committed
  9a2c532

  Copy full SHA for 9a2c532

• convert join to application

  tnelson

  committed
  e8a7c9f

  Copy full SHA for e8a7c9f

• add: allow Unknown message to Sterling; blank right now

  tnelson

  committed
  5ae8d8c

  Copy full SHA for 5ae8d8c

• defensive check

  tnelson

  committed
  b973852

  Copy full SHA for b973852

• more int work

  k-mouline

  committed
  0fb298a

  Copy full SHA for 0fb298a

• merge

  tnelson

  committed
  a8dec28

  Copy full SHA for a8dec28

Commits on Jul 4, 2024

• add: handle unknown in tests, etc. (cannot test much yet)

  tnelson

  committed
  ba285b2

  Copy full SHA for ba285b2

Commits on Jul 5, 2024

• to-skolem func args fixed

  k-mouline

  committed
  69c7123

  Copy full SHA for 69c7123

• fun spacer maintained in substitutor

  k-mouline

  committed
  0cda303

  Copy full SHA for 0cda303

• fix: error message string

  tnelson

  committed
  df80e05

  Copy full SHA for df80e05

• add: pair programming

  tnelson

  committed
  9358764

  Copy full SHA for 9358764

• add: comment only, thinking re: int

  tnelson

  committed
  a7534bb

  Copy full SHA for a7534bb

• add: Goldbach for unsat

  tnelson

  committed
  06d4100

  Copy full SHA for 06d4100

• Vars and decls sorted out

  k-mouline

  committed
  b614800

  Copy full SHA for b614800

Commits on Jul 8, 2024

• resolve conflict

  tnelson

  committed
  64d1b15

  Copy full SHA for 64d1b15

• fix: missing annotation #f

  tnelson

  committed
  a6574ce

  Copy full SHA for a6574ce

• add: annotation to qvar for smtlib integer conversion'

  tnelson

  committed
  972ba22

  Copy full SHA for 972ba22

• add: draft annotation use

  tnelson

  committed
  ae0d390

  Copy full SHA for ae0d390

• add: define sign SMT function, question re ints

  tnelson

  committed
  0fb841e

  Copy full SHA for 0fb841e

• add: comment, question about ints

  tnelson

  committed
  4e114a8

  Copy full SHA for 4e114a8

• add: untangle expr/const case

  tnelson

  committed
  26a74a2

  Copy full SHA for 26a74a2

• add: relational update unsupported

  tnelson

  committed
  6ae6ae9

  Copy full SHA for 6ae6ae9

• add: draft for translating none

  tnelson

  committed
  a4bfc03

  Copy full SHA for a4bfc03

• add: notes on int

  tnelson

  committed
  b874a48

  Copy full SHA for b874a48

• oops

  tnelson

  committed
  dfd6128

  Copy full SHA for dfd6128

• add: proof of concept, pair programming with Karim

  tnelson

  committed
  7c48a42

  Copy full SHA for 7c48a42

• add: stop policy to collector

  tnelson

  committed
  b54323c

  Copy full SHA for b54323c

Commits on Jul 9, 2024

• fix: hacky fix for substitutor fun-spacer; needs expanding

  tnelson

  committed
  87342b7

  Copy full SHA for 87342b7

• quantifier grounding added

  k-mouline

  committed
  32a92e0

  Copy full SHA for 32a92e0

• fake run added

  k-mouline

  committed
  efc57cf

  Copy full SHA for efc57cf

• fix: minor to collector, add grandpa

  tnelson

  committed
  a07b349

  Copy full SHA for a07b349

Commits on Aug 1, 2024

• Comparison pull request (#265)

  Show description for 80a1c1e
  

  k-mouline

  and

  tnelson

  authored
  80a1c1e

  Copy full SHA for 80a1c1e

• patch

  tnelson

  committed
  e0686e8

  Copy full SHA for e0686e8

• manual merge from dev

  tnelson

  committed
  37d99b6

  Copy full SHA for 37d99b6

• minor: comment change to avoid confusion

  tnelson

  committed
  cc08cd9

  Copy full SHA for cc08cd9

• minor: comment fix

  tnelson

  committed
  35e7e4b

  Copy full SHA for 35e7e4b

• fix: get-annotation for nodes

  tnelson

  committed
  0c3e9e5

  Copy full SHA for 0c3e9e5

Commits on Aug 5, 2024

• Fixing issue with to-smt visitor; refactor lang-specific error code (#267)

  tnelson

  authored
  2e22980

  Copy full SHA for 2e22980

• fix: quantifier case in tor conversion

  tnelson

  committed
  4cfef1a

  Copy full SHA for 4cfef1a

• fix: blocking in error case from cvc5

  tnelson

  committed
  7717a47

  Copy full SHA for 7717a47

• Comprehension and integer handling improved

  k-mouline

  committed
  d4509d5

  Copy full SHA for d4509d5

• fix: parsing smt response, allow 'some Node'

  tnelson

  committed
  f9e4855

  Copy full SHA for f9e4855

• rename univInt, no longer pass IntAtom-to-Int

  tnelson

  committed
  cbc2b61

  Copy full SHA for cbc2b61

Commits on Aug 6, 2024

• Cardinality supported, a few fixes needed

  k-mouline

  committed
  9e669dc

  Copy full SHA for 9e669dc

Commits on Aug 7, 2024

• match against nested ites

  tnelson

  committed
  9d4ed97

  Copy full SHA for 9d4ed97

• fix: issue with chained ite

  tnelson

  committed
  5a1adf3

  Copy full SHA for 5a1adf3

• fix: negative numbers in IntAtom-to-Int

  tnelson

  committed
  dfc5daa

  Copy full SHA for dfc5daa

• fix more

  tnelson

  committed
  ea152f2

  Copy full SHA for ea152f2

• fix: update sterling for larger numbers

  tnelson

  committed
  83e7bbc

  Copy full SHA for 83e7bbc

• Added more comp/card tests, added to expression-type struct

  k-mouline

  committed
  af90532

  Copy full SHA for af90532

Commits on Aug 8, 2024

• fix: remove leftover prints

  tnelson

  committed
  462edb1

  Copy full SHA for 462edb1

• fix: arity of function call

  tnelson

  committed
  7923a0d

  Copy full SHA for 7923a0d

• Tests for Tim

  k-mouline

  committed
  b05b7d5

  Copy full SHA for b05b7d5

• fix to use of 'second' in last-checker, clarifying comments

  tnelson

  committed
  4aae72f

  Copy full SHA for 4aae72f

• Multiplicities fixed and tests added

  k-mouline

  committed
  f3c86d4

  Copy full SHA for f3c86d4

Commits on Aug 12, 2024

• More tests

  k-mouline

  committed
  fa5b2e3

  Copy full SHA for fa5b2e3

Commits on Aug 14, 2024

• Relational override, reflexive tc typing, lone sig, and tests

  k-mouline

  committed
  48769bc

  Copy full SHA for 48769bc

• add: don't pass translation-helpers to sterling

  tnelson

  committed
  212463a

  Copy full SHA for 212463a

• Fixed cardinality of size 0 set typing

  k-mouline

  committed
  17cde9e

  Copy full SHA for 17cde9e

• Cardinality error fixed

  k-mouline

  committed
  dce6b19

  Copy full SHA for dce6b19

Commits on Aug 15, 2024

• add: finite int set, commented test example

  tnelson

  committed
  24a8905

  Copy full SHA for 24a8905

• add: additional comment

  tnelson

  committed
  1a23e3e

  Copy full SHA for 1a23e3e

Commits on Aug 16, 2024

• Plenty more tests added

  k-mouline

  committed
  b11ffa8

  Copy full SHA for b11ffa8

Commits on Aug 19, 2024

• Tests fixed

  k-mouline

  committed
  e9cbfeb

  Copy full SHA for e9cbfeb

Commits on Aug 20, 2024

• update pardinus: return parse error text

  tnelson

  committed
  3312ac6

  Copy full SHA for 3312ac6

• fix for non-smt, which gives no Int sig in instances

  tnelson

  committed
  2768b8b

  Copy full SHA for 2768b8b

• Feat smt s exp (#271)

  Show description for d91d825
  

  tnelson

  and

  k-mouline

  authored
  d91d825

  Copy full SHA for d91d825

• Fix prime check (#272)

  Show description for 4bcfe5b
  tnelson

  authored
  4bcfe5b

  Copy full SHA for 4bcfe5b

• Extra files removed

  k-mouline

  committed
  f167639

  Copy full SHA for f167639

• fix: skolemization tests robust to suffix

  tnelson

  committed
  8b62e4a

  Copy full SHA for 8b62e4a

Commits on Aug 21, 2024

• S-exp descent and substitution added

  k-mouline

  committed
  ff2ca40

  Copy full SHA for ff2ca40

• Small errors fixed

  k-mouline

  committed
  876db0e

  Copy full SHA for 876db0e

• refactor: SMT ToR tests into CI folder

  tnelson

  committed
  13c725b

  Copy full SHA for 13c725b

• Two out of three tests fixed

  k-mouline

  committed
  3d8df26

  Copy full SHA for 3d8df26

• remove outdated test

  tnelson

  committed
  2fefb34

  Copy full SHA for 2fefb34

• Temp file added for verbose SMT runs

  k-mouline

  committed
  cc34513

  Copy full SHA for cc34513

Commits on Aug 22, 2024

• cleanup verbosity, test cvc5 in CI

  tnelson

  committed
  f29b42c

  Copy full SHA for f29b42c

• experiment: actions

  tnelson

  committed
  8efdc1e

  Copy full SHA for 8efdc1e

• refine CI, update racket version and print cvc5 version

  tnelson

  committed
  c67df5e

  Copy full SHA for c67df5e

• Wrap negative numbers for earlier cvc5 versions

  tnelson

  committed
  6b961d2

  Copy full SHA for 6b961d2

• fix: wrap -1 in sign built-in

  tnelson

  committed
  7b068ed

  Copy full SHA for 7b068ed

• minor: cleanup

  tnelson

  committed
  e101a6d

  Copy full SHA for e101a6d

• add: more comprehension tests

  tnelson

  committed
  a9f2c6d

  Copy full SHA for a9f2c6d

• fix: uniqueness of ints, regression tests

  tnelson

  committed
  54fe251

  Copy full SHA for 54fe251

Commits on Aug 23, 2024

• add: understanding ic3 example

  tnelson

  committed
  da9777c

  Copy full SHA for da9777c

• fix: remainder lambda

  tnelson

  committed
  66f377d

  Copy full SHA for 66f377d

Commits on Sep 2, 2024

• minor fixes, mod

  tnelson

  committed
  d01c5a9

  Copy full SHA for d01c5a9

Commits on Sep 29, 2024

• add: avoid asserting true

  tnelson

  committed
  fe8d3e0

  Copy full SHA for fe8d3e0

• add: include options in SMT-lib, not command line, where applicable

  tnelson

  committed
  0c23720

  Copy full SHA for 0c23720

Commits on Oct 1, 2024

• add: simplify 'one' constraint

  tnelson

  committed
  60a292f

  Copy full SHA for 60a292f

Commits on Oct 15, 2024

• adjust CI

  tnelson

  committed
  61d7392

  Copy full SHA for 61d7392

• update: CI

  tnelson

  committed
  050b654

  Copy full SHA for 050b654

Commits on Oct 17, 2024

• smt tests verbosity set to 0

  k-mouline

  committed
  740b65b

  Copy full SHA for 740b65b

Commits on Oct 23, 2024

• add: improve debugging line in reader

  tnelson

  committed
  85ca793

  Copy full SHA for 85ca793

Commits on Nov 12, 2024

• add: exclude examples from domains from compile

  tnelson

  committed
  8fd9b3d

  Copy full SHA for 8fd9b3d

Commits on Nov 19, 2024

• Docker container for CI (#280)

  Show description for 9ef1c70
  k-mouline

  authored
  9ef1c70

  Copy full SHA for 9ef1c70

• add: null for PR in CI script

  tnelson

  committed
  ccc9da5

  Copy full SHA for ccc9da5

• Merge branch 'dev' into feat_smt

  tnelson

  authored
  d654466

  Copy full SHA for d654466

• update: continue reconciling dev with feature branch

  tnelson

  committed
  d1dbee2

  Copy full SHA for d1dbee2

• fix: is_theorem_disabled test, ++ case in smtlibtor conversion

  tnelson

  committed
  6d650ef

  Copy full SHA for 6d650ef

Commits on Nov 20, 2024

• cleanup: SMT / solver specifics

  tnelson

  committed
  82ca78a

  Copy full SHA for 82ca78a