diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2021-05-18 17:32:21 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-18 22:32:21 +0000 |
| commit | 47f71a6d94b600cf7c132569fa05ad1666edc408 (patch) | |
| tree | 3c4b244cd467f1ca888edfcf6edd5df358ce2aac /test/regress | |
| parent | c214051068aefdf831bf67e6b7d72591e5a91ece (diff) | |
Loop over terms to reconstruct instead of obligations. (#6504)
This PR modifies the rcons algorithm to loop over terms to reconstruct instead of obligations. It also modifies the Obs data structure to reflect this change. The rest of the PR is mostly updating documentation and refactoring the affected code.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress1/sygus/eq-sub-obs.sy | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/test/regress/regress1/sygus/eq-sub-obs.sy b/test/regress/regress1/sygus/eq-sub-obs.sy index 4c24a498d..69399e293 100644 --- a/test/regress/regress1/sygus/eq-sub-obs.sy +++ b/test/regress/regress1/sygus/eq-sub-obs.sy @@ -7,16 +7,21 @@ (set-logic UF) -(synth-fun f ((p Bool) (q Bool) (r Bool)) Bool +(synth-fun f ((p Bool) (q Bool) (r Bool) (s Bool)) Bool ((Start Bool)) - ((Start Bool (true false p q r (not Start) (and Start Start) (or Start Start))))) + ((Start Bool (p q r s (not Start) (and Start Start) + (or Start Start) (ite Start Start Start))))) -(define-fun eqReduce ((p Bool) (q Bool)) Bool (or (and p q) (and (not p) (not q)))) +(define-fun eqReduce ((p Bool) (q Bool)) Bool + (and (or p (not q)) (or (not p) q))) (declare-var p Bool) (declare-var q Bool) (declare-var r Bool) +(declare-var s Bool) -(constraint (= (f p q r) (and (= (and p q) (and q r)) (eqReduce (and p q) (and q r))))) +(constraint (= (f p q r s) (and (= (and p q) (and q r)) + (ite s (eqReduce (and p q) (and q r)) + (eqReduce (and p q) (and p r)))))) (check-synth) |