summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2015-03-10CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf ↵ajreynol
signature. Add regressions.
2015-03-05Minor fixes. Extend cegqi-si to real arithmetic.ajreynol
2015-03-04More work on arithmetic single invocation synthesis conjectures.ajreynol
2015-02-27Revert "dummy commit to force nightly builds"Kshitij Bansal
This reverts commit d2b44175c45a6d2c2fa9c3f8ec1ca1c433cb399b.
2015-02-26Robust strategy for single invocation LIA synthesis conjectures. Add ↵ajreynol
regressions.
2015-02-25Switch back to eager loop temporarily.Tianyi Liang
2015-02-24minor fix for internal string printTianyi Liang
2015-02-22New trigger options. --inst-no-entail on by default. Misc cleanup.ajreynol
2015-02-18dummy commit to force nightly buildsKshitij Bansal
2015-02-16Merge branch 'master' of https://github.com/CVC4/CVC4Kshitij Bansal
2015-02-16webget: curl follow redirectKshitij Bansal
2015-02-14Fix unit tests.ajreynol
2015-02-14attempt to fix win32 buildsKshitij Bansal
2015-02-13Minor cleanup, remove unused files.ajreynol
2015-02-13Handle recursive singleton case for codatatypes, add regression. Simplify ↵ajreynol
implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.
2015-02-12try curl before wget, workaround for issue with FTP PASVKshitij Bansal
2015-02-12Changing CXXFLAGS for custom cln installation in configure.ac.Tim King
Making sure the CVC4 flags do not get overwritten after being set.
2015-02-11Better support for solving multiple functions with cegqi-si. Minor cleanup.ajreynol
2015-02-11Move si solution reconstruction to own file, make more robust. Other ↵ajreynol
refactoring.
2015-02-06Handle missing cases for single inv solution reconstruction. Minor fixes. ↵ajreynol
Refactor.
2015-02-05Minor clean upTianyi Liang
2015-02-05Merge branch 'master' of github.com:tiliang/CVC4Tianyi Liang
2015-02-05Improved string performance, thanks to Peter's benchmarks.Tianyi Liang
2015-02-05Improved string performance, thanks to Peter's benchmarks.Tianyi Liang
2015-02-05Working version of sygus solution reconstruction from single inv cegqi. ↵ajreynol
Heuristics to fit syntax.
2015-02-04Initial draft of solution reconstruction into syntax for single inv cegqi.ajreynol
2015-02-04Work on solution reconstruction for single inv. Fix compiler error found by ↵ajreynol
Tim regarding Trace.isOn
2015-02-04Refactor sygus_util to TermDb. Initial work on solution reconstruction into ↵ajreynol
syntax for single inv properties.
2015-02-04Start work on simplifying single inv solutions. Minor.ajreynol
2015-02-03Simple variable elimination for single inv properties. Relax conditions for ↵ajreynol
partial inst variables for LTE.
2015-02-03Solutions for single invocation conjectures.ajreynol
2015-02-02Single invocation module for counterexample guided quantifier instantiation ↵ajreynol
--cegqi-si. Minor improvements to syntax-guided case, refactoring. Do not apply exhaustive tester inference for sygus datatypes.
2015-02-02Representative programs must be minimal size, minor fixes, improvements to ↵ajreynol
ITE handling in sygus.
2015-02-01Generalization of sygus lemmas based on arguments and content.ajreynol
2015-01-31Bug fix fairness for commutative operators in sygus. Minor.ajreynol
2015-01-31Lemmas instead of conflicts in sygus sym break (do not expand explanations). ↵ajreynol
Minor improvements to sygus splitting.
2015-01-30Generalize conflict clauses in sygus sym break, merge caches, refactor. ↵ajreynol
Preparation for single invocation properties. Set output lang to SMT2 for sygus.
2015-01-29Apply sygus search space narrowing for all subprograms of current global state.ajreynol
2015-01-29Restrict LtePartialInst instantiations based on E-matching, promote to ↵ajreynol
quantifiers module. Refactor QuantifiersEngine registration and check.
2015-01-29Apply global search space narrowing for multiple synth-fun, enable its ↵ajreynol
conflict lemmas.
2015-01-29Add module for sygus search space narrowing based on global state.ajreynol
2015-01-28Minor refactor CEGQI.ajreynol
2015-01-27Always miniscope nested quantifiers. Disable miniscoping when cegqi ↵ajreynol
enabled. Simplify option names.
2015-01-27Recognize when synthesis conjectures are in single invocation fragment.ajreynol
2015-01-26Output solutions for synthesis conjectures with --dump-synth. Minor ↵ajreynol
refactor of previous commit.
2015-01-26Generalize sygus search space narrowing to arbitrary theory rewriting.ajreynol
2015-01-24Variable patterns only look at eligible terms. Minor refactoring of ↵ajreynol
quantifiers check for sat.
2015-01-24Add --lte-restrict-inst-closure option. Push dt.size fairness constraints ↵ajreynol
inside splitting lemmas for sygus.
2015-01-23Refactor sygus arg nf. Minor improvements.ajreynol
2015-01-23CEGQI fairness based on term height. Fix sygus-nf fairness bug for wrongly ↵ajreynol
applied selectors.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback