summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2018-06-11Evaluator: support other theories for equalityeval3Andres Noetzli
2018-06-11Fix template.ajreynol
2018-06-11Evaluate templates.ajreynol
2018-06-11Merge pull request #4 from 4tXJ7f/eval2Andrew Reynolds
2018-06-11Add eval support for NOTAndres Noetzli
2018-06-11Merge pull request #3 from 4tXJ7f/evalAndrew Reynolds
2018-06-11FallbackevalAndres Noetzli
2018-06-11unit testAndres Noetzli
2018-06-11minor fixAndres Noetzli
2018-06-11More minorajreynol
2018-06-11Minorajreynol
2018-06-09EvaluatorAndres Noetzli
2018-06-09Minor fix for computing look-ahead conditionals in PBE i/o.ajreynol
2018-06-08Option for exclusion predicate, more BV rewrites.ajreynol
2018-06-07ITE bitvector rewrites.ajreynol
2018-06-07Remove polarity from ext rew theory passes.ajreynol
2018-06-07Make regression faster.ajreynol
2018-06-06Update CLIA script.ajreynol
2018-06-06Any failed function is full failure during reconstruction.ajreynol
2018-06-06Limit policy for reconstruction, remove all-abort cegqi-si.ajreynol
2018-06-06Formatajreynol
2018-06-06Options for reconstruction.ajreynol
2018-06-05Add missingajreynol
2018-06-05Subfield types, sol recons heuristics.ajreynol
2018-06-05Formatajreynol
2018-06-05Merge branch 'master' of https://github.com/CVC4/CVC4 into sygusComp2018-2ajreynol
2018-06-05Disable special case for all-abort Booleans.ajreynol
2018-06-05Simplify.ajreynol
2018-06-05Enable factoring, unit resolution.ajreynol
2018-06-04Only enable transcendentals if logic is N[I]RAT (#2052)Andres Noetzli
2018-06-04Work on factoring.ajreynol
2018-06-04More eq chain rewrites.ajreynol
2018-06-04Move assertion. (#2051)Andrew Reynolds
2018-06-04[SMT-COMP] Add new logics to run-scripts (#2022)Andres Noetzli
2018-06-04Enable cegqi (with model values) for floating point by default (#2023)Andrew Reynolds
2018-06-04Regressions: Support for requiring CVC4 features (#2044)Andres Noetzli
This commit adds supprt for the `REQUIRES` directive in our regression benchmarks. This directive can be used to enable certain benchmarks only if CVC4 has been configured with certain features enabled.
2018-06-02Revert reorg of relevancy conditions.ajreynol
2018-06-02 Fix assertion involving unassigned Boolean eqc in model (#2050)Andrew Reynolds
2018-06-02Fix corner case of mixed int/real cegqi. (#2046)Andrew Reynolds
2018-06-02Fix BV-abstraction check to consider SKOLEM. (#2042)Mathias Preiner
Further, fix a bug in the AIG bitblaster that was also uncovered with the minimized file.
2018-06-02Fix preinitialization pass for finite model finding (#2047)Andrew Reynolds
2018-06-01Add crcy regress.ajreynol
2018-06-01Fix quantified bv variable elimination (#2039)Andrew Reynolds
2018-06-01Fix quantifiers conflict lemma handling (#2043)Andrew Reynolds
2018-06-01Apply preprocessing to counterexample lemmas in CEGQI (#2027)Andrew Reynolds
2018-06-01 Use monomial sum utility to solve for quantifiers macros (#2038)Andrew Reynolds
2018-06-01Reorg relevancy conditions.ajreynol
2018-06-01Store negations of relevancy conditions.ajreynol
2018-06-01Formatajreynol
2018-06-01Cache substitute.ajreynol
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback