projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 338ec2e) | patch
Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding declare...
authorajreynol <andrew.j.reynolds@gmail.com>
Fri, 16 Jan 2015 11:38:08 +0000 (12:38 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Fri, 16 Jan 2015 11:38:08 +0000 (12:38 +0100)
commitcb54542531904204fc147015469d54c6750ab73b
treefa29a40d7a2761101bf2ce415e9682a9c238db6etree
parent338ec2ee86e16423b265ba9bfc036606223f846fcommit | diff
Allow uninterpreted/defined functions in Sygus grammars. Fix bug regarding declare-var vs synth-fun arguments.  Handle ground properties in sythesis conjectures.
src/parser/smt2/Smt2.g diff | blob | history
src/parser/smt2/smt2.h diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.cpp diff | blob | history
src/theory/quantifiers/ce_guided_instantiation.h diff | blob | history
src/theory/quantifiers/options diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history