cvc5.git
9 years agoFix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions.
ajreynol [Tue, 21 Apr 2015 14:34:56 +0000 (16:34 +0200)]
Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions.

9 years agoAdding an example of a tester in SMT2.
Tim King [Tue, 21 Apr 2015 07:55:11 +0000 (09:55 +0200)]
Adding an example of a tester in SMT2.

9 years agoFarkas proof coefficients.
Tim King [Fri, 17 Apr 2015 13:22:53 +0000 (15:22 +0200)]
Farkas proof coefficients.

This commit adds tracking of Farkas coefficients to proof enabled builds in the theory of linear
real arithmetic when proofs are enabled. There could be some performance changes due to subtly
different search paths being taken.

Additional bug fixes:
- Polynomial::exactDivide did not satisfy preconditions to the Monomial constructor.
  To prevent future problems, Monomials should now be made via one of the mkMonomial functions.
- Fixes a bug in SumOfInfeasibilitiesSPD::greedyConflictSubsets().
  There was a way to use a row twice in the construction of the conflicts.
  This was violating an assumption in the Tableau when constructing the intermediate rows.

Constraints:
- To enable proofs, all conflicts and propagations are designed to go through the Constraint system
  before they are converted to externally understandable conflicts and propagations in the form
  of Node.
- Constraints must now be given a reason for marking them as true that corresponds to a proof.
- Constraints should now be marked as being true by one of the impliedbyX functions.
- Each impliedByX function has an ArithProofType associated with it.
- Each call to an impliedByX function stores a context dependent ConstraintRule object
  to track the proof.
- After marking the node as true the caller should either try to propagate the constraint or raise
a conflict.
- There are no more special cases for marking a node as being true when its negation has a proof
  vs. when the negation does not have a proof. One must now explicitly pass in a inConflict flag
to the impliedByX (and similar functions).
For example,this is now longer both:
  void setAssertedToTheTheory(TNode witness);
  void setAssertedToTheTheoryWithNegationTrue(TNode witness);
  There is just:
    void setAssertedToTheTheory(TNode witness, bool inConflict);

9 years agoPatch for Kshitij's fix on requriePhase
Tianyi Liang [Fri, 17 Apr 2015 19:41:24 +0000 (14:41 -0500)]
Patch for Kshitij's fix on requriePhase

9 years agoMerge pull request #72 from kbansal/decision-requirephase
Kshitij Bansal [Fri, 17 Apr 2015 18:43:20 +0000 (14:43 -0400)]
Merge pull request #72 from kbansal/decision-requirephase

https://www.starexec.org/starexec/secure/details/job.jsp?id=6972

The plot is bit misleading. Those not on x=y, are from QF_BV/asp which are segfaulting (see bugzilla 623). No performance impact on other logics it was tested on.

9 years agoFix option --quant-fun-wd. Add mk_starexec script to contrib.
ajreynol [Thu, 16 Apr 2015 10:34:27 +0000 (12:34 +0200)]
Fix option --quant-fun-wd.  Add mk_starexec script to contrib.

9 years agoHandle (degenerate) case of synthesis conjectures for constants. Disable delta lemmas.
ajreynol [Thu, 16 Apr 2015 09:21:07 +0000 (11:21 +0200)]
Handle (degenerate) case of synthesis conjectures for constants.  Disable delta lemmas.

9 years agoEnabling the regression test: test/regress/regress0/unconstrained/mult1.smt2
Tim King [Wed, 15 Apr 2015 19:34:37 +0000 (21:34 +0200)]
Enabling the regression test: test/regress/regress0/unconstrained/mult1.smt2

9 years agoFix for unconstrained bug.
Clark Barrett [Wed, 15 Apr 2015 19:20:13 +0000 (12:20 -0700)]
Fix for unconstrained bug.

9 years agoAdding an example that violates an assertion during unconstrained simplification.
Tim King [Wed, 15 Apr 2015 16:10:43 +0000 (18:10 +0200)]
Adding an example that violates an assertion during unconstrained simplification.

9 years agoMaking CVC4::theory::quantifiers::PrenexQuantMode public for now.
Tim King [Mon, 13 Apr 2015 10:23:49 +0000 (12:23 +0200)]
Making CVC4::theory::quantifiers::PrenexQuantMode public for now.

9 years agodisable string reqressions timing out after change
Kshitij Bansal [Thu, 9 Apr 2015 20:25:01 +0000 (16:25 -0400)]
disable string reqressions timing out after change

9 years agoDE requests respect requirePhase
Kshitij Bansal [Thu, 9 Apr 2015 19:48:25 +0000 (15:48 -0400)]
DE requests respect requirePhase

9 years agoFix unsat-core issues related to rewrite rules, quantifiers preprocessing, and string...
ajreynol [Thu, 9 Apr 2015 13:51:26 +0000 (15:51 +0200)]
Fix unsat-core issues related to rewrite rules, quantifiers preprocessing, and strings preprocessing.  Minor fix for conjecture generation for finite types.

9 years agoFix performance issue with variable triggers + instantiation restrictions.
ajreynol [Thu, 9 Apr 2015 10:43:37 +0000 (12:43 +0200)]
Fix performance issue with variable triggers + instantiation restrictions.

9 years agoBug fix negative contains cache.
ajreynol [Thu, 9 Apr 2015 09:35:33 +0000 (11:35 +0200)]
Bug fix negative contains cache.

9 years agoMake fun-def quantifiers carry the function app they define, make fun-def utilities...
ajreynol [Wed, 8 Apr 2015 10:15:27 +0000 (12:15 +0200)]
Make fun-def quantifiers carry the function app they define, make fun-def utilities more robust.  Fix bug in conjecture generation for non-parameterized operators.

9 years agoRemoving the reference to THEORY_BOOL from the equality engine. This theory
Dejan Jovanovic [Wed, 8 Apr 2015 06:48:57 +0000 (23:48 -0700)]
Removing the reference to THEORY_BOOL from the equality engine. This theory
id was used as an internal marker in a set of theories tagging reasons of a
propagated disequalities. Replaced it with THEORY_LAST which is not completely
kosher but is safe in the context being used.

9 years agoMinor fixes for cegqi.
ajreynol [Tue, 7 Apr 2015 09:37:24 +0000 (11:37 +0200)]
Minor fixes for cegqi.

9 years agoMerge pull request #71 from kbansal/const-are-triggers
Kshitij Bansal [Thu, 2 Apr 2015 17:05:31 +0000 (13:05 -0400)]
Merge pull request #71 from kbansal/const-are-triggers

change const are triggers from false to true in equality engines

Performance comparison:
   https://www.starexec.org/starexec/secure/details/job.jsp?id=6941

Bug opened for testcase that became much worse:
  http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=621

9 years agoImprovements and bug fixes related to cbqi/cegqi. Minor fix for fmf with fun-def...
ajreynol [Wed, 1 Apr 2015 11:09:49 +0000 (13:09 +0200)]
Improvements and bug fixes related to cbqi/cegqi.  Minor fix for fmf with fun-def. Add skolemization options.

9 years agofix no return value warning
Kshitij Bansal [Tue, 31 Mar 2015 23:26:27 +0000 (19:26 -0400)]
fix no return value warning

9 years agofix echo command in --tear-down-incremental
Kshitij Bansal [Tue, 31 Mar 2015 23:26:06 +0000 (19:26 -0400)]
fix echo command in --tear-down-incremental

9 years agoprinter change for string smtlib2
Tianyi Liang [Sat, 28 Mar 2015 17:04:33 +0000 (12:04 -0500)]
printer change for string smtlib2

9 years agochange const are triggers from false to true in equality engines
Kshitij Bansal [Wed, 25 Mar 2015 19:04:10 +0000 (15:04 -0400)]
change const are triggers from false to true in equality engines

9 years agoParsing support for define-fun-rec/define-funs-rec.
ajreynol [Mon, 23 Mar 2015 16:54:55 +0000 (17:54 +0100)]
Parsing support for define-fun-rec/define-funs-rec.

9 years agoDecouple counter-example guided quantifier instantiation from Sygus.
ajreynol [Mon, 23 Mar 2015 14:09:25 +0000 (15:09 +0100)]
Decouple counter-example guided quantifier instantiation from Sygus.

9 years agoAdd requirePhase len(x) = 0.
Tianyi Liang [Mon, 16 Mar 2015 16:04:43 +0000 (11:04 -0500)]
Add requirePhase len(x) = 0.

9 years agoFixed proof unitialized memory and minor memory leaks.
Liana Hadarean [Mon, 16 Mar 2015 13:31:21 +0000 (14:31 +0100)]
Fixed proof unitialized memory and minor memory leaks.

9 years agoBug fix for BV
Tianyi Liang [Sat, 14 Mar 2015 22:33:26 +0000 (17:33 -0500)]
Bug fix for BV

9 years agoPatches for 32-bit ARM
Tianyi Liang [Sat, 14 Mar 2015 22:25:17 +0000 (17:25 -0500)]
Patches for 32-bit ARM

9 years agoUpdating resize for occurence lists to properly resize the whole state.
Dejan Jovanovic [Sat, 14 Mar 2015 07:24:24 +0000 (00:24 -0700)]
Updating resize for occurence lists to properly resize the whole state.

9 years agoStrings split on constant lengths, add length=0 to split lemma for empty string.
ajreynol [Wed, 11 Mar 2015 20:11:20 +0000 (21:11 +0100)]
Strings split on constant lengths, add length=0 to split lemma for empty string.

9 years agoMinor fixes and improvements to cegqi-si for linear arithmetic.
ajreynol [Wed, 11 Mar 2015 14:43:56 +0000 (15:43 +0100)]
Minor fixes and improvements to cegqi-si for linear arithmetic.

9 years agoCNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf signature...
ajreynol [Tue, 10 Mar 2015 14:15:26 +0000 (15:15 +0100)]
CNF proofs.  Infrastructure for preprocessing proofs.  Updates to smt.plf signature.  Add regressions.

9 years agoMinor fixes. Extend cegqi-si to real arithmetic.
ajreynol [Thu, 5 Mar 2015 13:59:15 +0000 (14:59 +0100)]
Minor fixes.  Extend cegqi-si to real arithmetic.

9 years agoMore work on arithmetic single invocation synthesis conjectures.
ajreynol [Wed, 4 Mar 2015 09:39:27 +0000 (10:39 +0100)]
More work on arithmetic single invocation synthesis conjectures.

9 years agoRevert "dummy commit to force nightly builds"
Kshitij Bansal [Sat, 28 Feb 2015 02:47:09 +0000 (21:47 -0500)]
Revert "dummy commit to force nightly builds"

This reverts commit d2b44175c45a6d2c2fa9c3f8ec1ca1c433cb399b.

9 years agoRobust strategy for single invocation LIA synthesis conjectures. Add regressions.
ajreynol [Thu, 26 Feb 2015 14:16:15 +0000 (15:16 +0100)]
Robust strategy for single invocation LIA synthesis conjectures.  Add regressions.

9 years agoSwitch back to eager loop temporarily.
Tianyi Liang [Wed, 25 Feb 2015 16:49:14 +0000 (10:49 -0600)]
Switch back to eager loop temporarily.

9 years agominor fix for internal string print
Tianyi Liang [Wed, 25 Feb 2015 04:13:28 +0000 (22:13 -0600)]
minor fix for internal string print

9 years agoNew trigger options. --inst-no-entail on by default. Misc cleanup.
ajreynol [Sun, 22 Feb 2015 07:59:03 +0000 (08:59 +0100)]
New trigger options.  --inst-no-entail on by default.  Misc cleanup.

9 years agodummy commit to force nightly builds
Kshitij Bansal [Thu, 19 Feb 2015 04:48:35 +0000 (23:48 -0500)]
dummy commit to force nightly builds

9 years agoMerge branch 'master' of https://github.com/CVC4/CVC4
Kshitij Bansal [Mon, 16 Feb 2015 06:54:31 +0000 (01:54 -0500)]
Merge branch 'master' of https://github.com/CVC4/CVC4

9 years agowebget: curl follow redirect
Kshitij Bansal [Mon, 16 Feb 2015 06:54:27 +0000 (01:54 -0500)]
webget: curl follow redirect

9 years agoFix unit tests.
ajreynol [Sat, 14 Feb 2015 10:47:03 +0000 (11:47 +0100)]
Fix unit tests.

9 years agoattempt to fix win32 builds
Kshitij Bansal [Sat, 14 Feb 2015 10:21:28 +0000 (05:21 -0500)]
attempt to fix win32 builds

9 years agoMinor cleanup, remove unused files.
ajreynol [Fri, 13 Feb 2015 13:59:42 +0000 (14:59 +0100)]
Minor cleanup, remove unused files.

9 years agoHandle recursive singleton case for codatatypes, add regression. Simplify implementa...
ajreynol [Fri, 13 Feb 2015 13:12:32 +0000 (14:12 +0100)]
Handle recursive singleton case for codatatypes, add regression.  Simplify implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.

9 years agotry curl before wget, workaround for issue with FTP PASV
Kshitij Bansal [Thu, 12 Feb 2015 13:49:50 +0000 (08:49 -0500)]
try curl before wget, workaround for issue with FTP PASV

9 years agoChanging CXXFLAGS for custom cln installation in configure.ac.
Tim King [Thu, 12 Feb 2015 11:04:57 +0000 (12:04 +0100)]
Changing CXXFLAGS for custom cln installation in configure.ac.

Making sure the CVC4 flags do not get overwritten after being set.

9 years agoBetter support for solving multiple functions with cegqi-si. Minor cleanup.
ajreynol [Wed, 11 Feb 2015 18:07:49 +0000 (19:07 +0100)]
Better support for solving multiple functions with cegqi-si.  Minor cleanup.

9 years agoMove si solution reconstruction to own file, make more robust. Other refactoring.
ajreynol [Wed, 11 Feb 2015 12:10:11 +0000 (13:10 +0100)]
Move si solution reconstruction to own file, make more robust. Other refactoring.

9 years agoHandle missing cases for single inv solution reconstruction. Minor fixes. Refactor.
ajreynol [Fri, 6 Feb 2015 08:35:49 +0000 (09:35 +0100)]
Handle missing cases for single inv solution reconstruction.  Minor fixes. Refactor.

9 years agoMinor clean up
Tianyi Liang [Fri, 6 Feb 2015 00:42:08 +0000 (18:42 -0600)]
Minor clean up

9 years agoMerge branch 'master' of github.com:tiliang/CVC4
Tianyi Liang [Fri, 6 Feb 2015 00:29:06 +0000 (18:29 -0600)]
Merge branch 'master' of github.com:tiliang/CVC4

9 years agoImproved string performance, thanks to Peter's benchmarks.
Tianyi Liang [Fri, 6 Feb 2015 00:27:47 +0000 (18:27 -0600)]
Improved string performance, thanks to Peter's benchmarks.

9 years agoImproved string performance, thanks to Peter's benchmarks.
Tianyi Liang [Fri, 6 Feb 2015 00:27:47 +0000 (18:27 -0600)]
Improved string performance, thanks to Peter's benchmarks.

9 years agoWorking version of sygus solution reconstruction from single inv cegqi. Heuristics...
ajreynol [Thu, 5 Feb 2015 13:50:09 +0000 (14:50 +0100)]
Working version of sygus solution reconstruction from single inv cegqi.  Heuristics to fit syntax.

9 years agoInitial draft of solution reconstruction into syntax for single inv cegqi.
ajreynol [Wed, 4 Feb 2015 21:16:45 +0000 (22:16 +0100)]
Initial draft of solution reconstruction into syntax for single inv cegqi.

9 years agoWork on solution reconstruction for single inv. Fix compiler error found by Tim...
ajreynol [Wed, 4 Feb 2015 14:25:16 +0000 (15:25 +0100)]
Work on solution reconstruction for single inv.  Fix compiler error found by Tim regarding Trace.isOn

9 years agoRefactor sygus_util to TermDb. Initial work on solution reconstruction into syntax...
ajreynol [Wed, 4 Feb 2015 12:29:28 +0000 (13:29 +0100)]
Refactor sygus_util to TermDb.  Initial work on solution reconstruction into syntax for single inv properties.

9 years agoStart work on simplifying single inv solutions. Minor.
ajreynol [Wed, 4 Feb 2015 08:19:46 +0000 (09:19 +0100)]
Start work on simplifying single inv solutions.  Minor.

9 years agoSimple variable elimination for single inv properties. Relax conditions for partial...
ajreynol [Tue, 3 Feb 2015 10:39:03 +0000 (11:39 +0100)]
Simple variable elimination for single inv properties.  Relax conditions for partial inst variables for LTE.

9 years agoSolutions for single invocation conjectures.
ajreynol [Mon, 2 Feb 2015 23:21:52 +0000 (00:21 +0100)]
Solutions for single invocation conjectures.

9 years agoSingle invocation module for counterexample guided quantifier instantiation --cegqi...
ajreynol [Mon, 2 Feb 2015 16:42:31 +0000 (17:42 +0100)]
Single invocation module for counterexample guided quantifier instantiation --cegqi-si. Minor improvements to syntax-guided case, refactoring.  Do not apply exhaustive tester inference for sygus datatypes.

9 years agoRepresentative programs must be minimal size, minor fixes, improvements to ITE handli...
ajreynol [Mon, 2 Feb 2015 07:48:51 +0000 (08:48 +0100)]
Representative programs must be minimal size, minor fixes, improvements to ITE handling in sygus.

9 years agoGeneralization of sygus lemmas based on arguments and content.
ajreynol [Sun, 1 Feb 2015 19:54:28 +0000 (20:54 +0100)]
Generalization of sygus lemmas based on arguments and content.

9 years agoBug fix fairness for commutative operators in sygus. Minor.
ajreynol [Sat, 31 Jan 2015 17:50:01 +0000 (18:50 +0100)]
Bug fix fairness for commutative operators in sygus.  Minor.

9 years agoLemmas instead of conflicts in sygus sym break (do not expand explanations). Minor...
ajreynol [Sat, 31 Jan 2015 10:12:09 +0000 (11:12 +0100)]
Lemmas instead of conflicts in sygus sym break (do not expand explanations).  Minor improvements to sygus splitting.

9 years agoGeneralize conflict clauses in sygus sym break, merge caches, refactor. Preparation...
ajreynol [Fri, 30 Jan 2015 19:59:05 +0000 (20:59 +0100)]
Generalize conflict clauses in sygus sym break, merge caches, refactor.  Preparation for single invocation properties.  Set output lang to SMT2 for sygus.

9 years agoApply sygus search space narrowing for all subprograms of current global state.
ajreynol [Thu, 29 Jan 2015 16:09:21 +0000 (17:09 +0100)]
Apply sygus search space narrowing for all subprograms of current global state.

9 years agoRestrict LtePartialInst instantiations based on E-matching, promote to quantifiers...
ajreynol [Thu, 29 Jan 2015 12:08:31 +0000 (13:08 +0100)]
Restrict LtePartialInst instantiations based on E-matching, promote to quantifiers module.  Refactor QuantifiersEngine registration and check.

9 years agoApply global search space narrowing for multiple synth-fun, enable its conflict lemmas.
ajreynol [Thu, 29 Jan 2015 09:17:58 +0000 (10:17 +0100)]
Apply global search space narrowing for multiple synth-fun, enable its conflict lemmas.

9 years agoAdd module for sygus search space narrowing based on global state.
ajreynol [Thu, 29 Jan 2015 07:27:18 +0000 (08:27 +0100)]
Add module for sygus search space narrowing based on global state.

9 years agoMinor refactor CEGQI.
ajreynol [Wed, 28 Jan 2015 14:21:21 +0000 (15:21 +0100)]
Minor refactor CEGQI.

9 years agoAlways miniscope nested quantifiers. Disable miniscoping when cegqi enabled. Simpli...
ajreynol [Tue, 27 Jan 2015 17:17:27 +0000 (18:17 +0100)]
Always miniscope nested quantifiers.  Disable miniscoping when cegqi enabled.  Simplify option names.

9 years agoRecognize when synthesis conjectures are in single invocation fragment.
ajreynol [Tue, 27 Jan 2015 13:09:32 +0000 (14:09 +0100)]
Recognize when synthesis conjectures are in single invocation fragment.

9 years agoOutput solutions for synthesis conjectures with --dump-synth. Minor refactor of...
ajreynol [Mon, 26 Jan 2015 12:11:01 +0000 (13:11 +0100)]
Output solutions for synthesis conjectures with --dump-synth.  Minor refactor of previous commit.

9 years agoGeneralize sygus search space narrowing to arbitrary theory rewriting.
ajreynol [Mon, 26 Jan 2015 09:41:51 +0000 (10:41 +0100)]
Generalize sygus search space narrowing to arbitrary theory rewriting.

9 years agoVariable patterns only look at eligible terms. Minor refactoring of quantifiers...
ajreynol [Sat, 24 Jan 2015 18:42:21 +0000 (19:42 +0100)]
Variable patterns only look at eligible terms.  Minor refactoring of quantifiers check for sat.

9 years agoAdd --lte-restrict-inst-closure option. Push dt.size fairness constraints inside...
ajreynol [Sat, 24 Jan 2015 18:00:59 +0000 (19:00 +0100)]
Add --lte-restrict-inst-closure option.  Push dt.size fairness constraints inside splitting lemmas for sygus.

9 years agoRefactor sygus arg nf. Minor improvements.
ajreynol [Fri, 23 Jan 2015 19:40:57 +0000 (20:40 +0100)]
Refactor sygus arg nf.  Minor improvements.

9 years agoCEGQI fairness based on term height. Fix sygus-nf fairness bug for wrongly applied...
ajreynol [Fri, 23 Jan 2015 13:53:19 +0000 (14:53 +0100)]
CEGQI fairness based on term height.  Fix sygus-nf fairness bug for wrongly applied selectors.

9 years agoRework inst-closure.
ajreynol [Fri, 23 Jan 2015 09:04:38 +0000 (10:04 +0100)]
Rework inst-closure.

9 years agoNarrow sygus search space based on NNF and rewriting constant arguments.
ajreynol [Thu, 22 Jan 2015 16:09:29 +0000 (17:09 +0100)]
Narrow sygus search space based on NNF and rewriting constant arguments.

9 years agoAdd option --lte-partial-inst. Remove inst-closure.
ajreynol [Thu, 22 Jan 2015 10:47:39 +0000 (11:47 +0100)]
Add option --lte-partial-inst.  Remove inst-closure.

9 years agoDo not drop patterns during boolean term rewriting. Narrow sygus search space based...
ajreynol [Thu, 22 Jan 2015 08:40:51 +0000 (09:40 +0100)]
Do not drop patterns during boolean term rewriting. Narrow sygus search space based on commutative operators.

9 years agoAvoid redundant constant arguments for SygusNormalForm. Refactor.
ajreynol [Wed, 21 Jan 2015 14:44:27 +0000 (15:44 +0100)]
Avoid redundant constant arguments for SygusNormalForm. Refactor.

9 years agoInitial work on sygusNormalForm.
ajreynol [Wed, 21 Jan 2015 10:34:55 +0000 (11:34 +0100)]
Initial work on sygusNormalForm.

9 years agoMark datatypes as sygus. Add option to normalize sygus terms in search. Add sygus...
ajreynol [Tue, 20 Jan 2015 13:23:04 +0000 (14:23 +0100)]
Mark datatypes as sygus.  Add option to normalize sygus terms in search.  Add sygus regressions.

9 years agoHandle miniscoping of conjunctions in synthesis properties. Refactor construction...
ajreynol [Tue, 20 Jan 2015 09:23:08 +0000 (10:23 +0100)]
Handle miniscoping of conjunctions in synthesis properties.  Refactor construction of sygus datatypes.  Expand define-fun in evaluators.

9 years agoAdding tests for get-value output for arithmetic.
Tim King [Mon, 19 Jan 2015 17:57:29 +0000 (18:57 +0100)]
Adding tests for get-value output for arithmetic.

Fixing bug where (- 1).0 was printed by get-value. Thanks to Christoph Sticksel for the bug report.

9 years agoAdding an additional search path to configure.ac for cxxtestgen to reflect the cxxtes...
Tim King [Fri, 16 Jan 2015 10:31:33 +0000 (11:31 +0100)]
Adding an additional search path to configure.ac for cxxtestgen to reflect the cxxtest git repository.

9 years agoAvoid name conflicts for multiple synth-fun.
ajreynol [Sat, 17 Jan 2015 10:01:32 +0000 (11:01 +0100)]
Avoid name conflicts for multiple synth-fun.

9 years agoLinearize multiplication by constants in sygus grammars. Handle unary minus integer...
ajreynol [Fri, 16 Jan 2015 16:17:56 +0000 (17:17 +0100)]
Linearize multiplication by constants in sygus grammars. Handle unary minus integer numerals.  Refactor to smt2.cpp.

9 years agoAllow uninterpreted/defined functions in Sygus grammars. Fix bug regarding declare...
ajreynol [Fri, 16 Jan 2015 11:38:08 +0000 (12:38 +0100)]
Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding declare-var vs synth-fun arguments.  Handle ground properties in sythesis conjectures.

9 years agoMinor: Ensure indexed terms are in EE. Add support for bv constants in sygus parser.
ajreynol [Fri, 16 Jan 2015 08:29:15 +0000 (09:29 +0100)]
Minor: Ensure indexed terms are in EE.  Add support for bv constants in sygus parser.

9 years agosygus input language and benchmark
Morgan Deters [Fri, 24 Oct 2014 00:58:08 +0000 (20:58 -0400)]
sygus input language and benchmark

9 years agoFix #line numbering.
Morgan Deters [Tue, 13 Jan 2015 20:00:31 +0000 (15:00 -0500)]
Fix #line numbering.