projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Eliminating static calls to rewriter from strings (#7302)
[cvc5.git] / src / theory / quantifiers /
2021-10-01 Aina NiemetzRename SmtEngine to SolverEngine. (#7282) tree | commitdiff
2021-09-30 Aina NiemetzRename files smt_engine.(cpp|h) to solver_engine.(cpp... tree | commitdiff
2021-09-29 Andrew ReynoldsProperly restrict PBE symmetry breaking for abduction... tree | commitdiff
2021-09-24 Andrew ReynoldsEliminate calls to Rewriter::rewrite from strings entai... tree | commitdiff
2021-09-23 Gereon KremerEliminate Output macro in favor of simple Env functions... tree | commitdiff
2021-09-23 Andrew ReynoldsImplement alpha equivalence proofs (#7066) tree | commitdiff
2021-09-22 Andrew ReynoldsMake cegqi subsolvers EnvObj (#7205) tree | commitdiff
2021-09-22 Andrew ReynoldsTowards standard usage of evaluator (#7189) tree | commitdiff
2021-09-16 Andrew ReynoldsFix relevant domain for parametric operators (#7198) tree | commitdiff
2021-09-15 Andrew ReynoldsMinor changes to E-matching utilities (#7062) tree | commitdiff
2021-09-15 Andrew ReynoldsEliminate global access to options:: from quantifiers... tree | commitdiff
2021-09-13 Andres NoetzliRemove context getters from `TheoryState` (#7174) tree | commitdiff
2021-09-10 Andres NoetzliUse C++17 attributes (#7154) tree | commitdiff
2021-09-09 Andres NoetzliRemove `TheoryState::getEnv()` (#7163) tree | commitdiff
2021-09-09 Andrew ReynoldsDisable shared selectors for quantified logics without... tree | commitdiff
2021-09-09 Andres NoetzliRemove `TheoryState::options()` (#7148) tree | commitdiff
2021-09-09 Andrew ReynoldsRemove deprecated SyGuS method evaluateWithUnfolding... tree | commitdiff
2021-09-08 Andrew ReynoldsImprove pre-skolemization, move quantifiers preprocess... tree | commitdiff
2021-09-08 Andrew ReynoldsTowards standard usage of ExtendedRewriter (#7145) tree | commitdiff
2021-09-07 Andres NoetzliUse `EnvObj` methods instead of `Theory` methods (... tree | commitdiff
2021-09-07 Aina Niemetzsygus: Eliminate calls to Rewriter::rewrite. (#7142) tree | commitdiff
2021-09-03 Aina NiemetzEnvObj: Add options(), context(), userContext(). (... tree | commitdiff
2021-09-03 MikolasJanotaAvoiding duplicate search in maps (#7055) tree | commitdiff
2021-09-03 Aina Niemetzsygus: Make more classes derive from EnvObj. (#7140) tree | commitdiff
2021-09-03 Andrew ReynoldsMake quantifier module classes derive from EnvObj ... tree | commitdiff
2021-09-03 Aina Niemetzsygus: Make CeSingleInv derive from EnvObj. (#7136) tree | commitdiff
2021-09-02 Andrew ReynoldsRemove more instances of ufHo (#7087) tree | commitdiff
2021-09-02 Aina Niemetzrewriter: Make rewriteEqualityExt non-static. (#7110) tree | commitdiff
2021-08-30 Andrew ReynoldsFix quantifiers dynamic split module for parametric... tree | commitdiff
2021-08-27 Andrew ReynoldsExpand definitions in sygus operators at the SMT level... tree | commitdiff
2021-08-26 Andrew ReynoldsEliminate currentSmtEngine for subsolver calls (#7068) tree | commitdiff
2021-08-26 Andrew ReynoldsMake datatype selector expansion to its own accessible... tree | commitdiff
2021-08-26 Gereon KremerConsolidate language types (#7065) tree | commitdiff
2021-08-25 Andrew ReynoldsEliminate calls to currentSmtEngine (#7060) tree | commitdiff
2021-08-24 Andrew ReynoldsSplit higher-order term database (#7045) tree | commitdiff
2021-08-24 Andrew ReynoldsRefactor enumerator management in synth conjecture... tree | commitdiff
2021-08-23 Andrew ReynoldsFix non-deterministism in quantified datatypes expansio... tree | commitdiff
2021-08-23 Andrew ReynoldsGeneralize inequality elimination in quantifiers rewrit... tree | commitdiff
2021-08-23 Andrew ReynoldsFix single invocation partition for higher-order (... tree | commitdiff
2021-08-22 Andrew ReynoldsPrenex quantified formulas with user annotations by... tree | commitdiff
2021-08-20 Andrew ReynoldsSimplify how user-provided quantifier attributes are... tree | commitdiff
2021-08-20 Andrew ReynoldsMore refactoring of set defaults (#7043) tree | commitdiff
2021-08-18 Andres NoetzliMinor fixes of policy for eliminating quantifiers ... tree | commitdiff
2021-08-17 Andrew ReynoldsRefactoring theory-specific variable elimination in... tree | commitdiff
2021-08-17 Andrew ReynoldsFix policy for eliminating quantified formulas (#7017) tree | commitdiff
2021-08-17 Andrew ReynoldsImprove conversion to skolems in expression miner ... tree | commitdiff
2021-08-17 Gereon KremerPush Env class into TheoryState (#7012) tree | commitdiff
2021-08-16 Gereon KremerMake Theory class use Env (#7011) tree | commitdiff
2021-08-04 Andrew ReynoldsAdd inference ids for remainder of sygus solver (#6977) tree | commitdiff
2021-08-04 Mathias Preinersyqi: Add debug information for dumping instantiations... tree | commitdiff
2021-08-04 Andrew ReynoldsAdd optional debug information for dumping instantiatio... tree | commitdiff
2021-08-04 Andrew ReynoldsAdd missing inference identifiers (#6962) tree | commitdiff
2021-07-28 Andrew ReynoldsMake extended rewriter methods const (#6948) tree | commitdiff
2021-07-27 Andrew ReynoldsTrack instantiation reasons in proofs (#6935) tree | commitdiff
2021-07-27 Andrew ReynoldsMove enum value generator to own file (#6941) tree | commitdiff
2021-07-27 Andrew ReynoldsMinor fix for term database + central equality engine... tree | commitdiff
2021-07-27 Andrew ReynoldsMake all dependencies in the fast enumerator optional... tree | commitdiff
2021-07-27 Andrew ReynoldsAdd sygus enumerator callback (#6923) tree | commitdiff
2021-07-16 Andrew ReynoldsDo not exhaustive instantiation when FMF is disabled... tree | commitdiff
2021-07-15 Andrew ReynoldsFix context for proofs of instantiations (#6890) tree | commitdiff
2021-07-15 Andrew ReynoldsDistinguish quantifiers preprocess as its own proof... tree | commitdiff
2021-07-15 Andrew ReynoldsMove master equality engine notification to own file... tree | commitdiff
2021-07-14 Andrew ReynoldsMove synthesis verification check to own file (#6882) tree | commitdiff
2021-07-07 Andrew ReynoldsStandard output for trigger selection (#6841) tree | commitdiff
2021-07-03 Andres NoetzliFix performance of string regression (#6832) tree | commitdiff
2021-07-03 Mathias PreinerAdd output tags -o, --output. (#6826) tree | commitdiff
2021-07-01 Andrew ReynoldsAdd recursive function definitions to subsolver in... tree | commitdiff
2021-07-01 Andrew ReynoldsAdd option to limit the number of instantiation rounds... tree | commitdiff
2021-06-30 Andrew ReynoldsDo not apply fmfBound to standard quantifiers when... tree | commitdiff
2021-06-28 Andrew ReynoldsRename internal string kinds to match API (#6797) tree | commitdiff
2021-06-22 Andrew ReynoldsFix type enumeration for non first-class sorts in FMF... tree | commitdiff
2021-06-15 Gereon KremerRemove public option wrappers (#6716) tree | commitdiff
2021-06-08 Andrew ReynoldsFix for 2 dimensional dependent bounded quantifiers... tree | commitdiff
2021-06-07 Gereon KremerRemove `Options::wasSetByUser()` (#6682) tree | commitdiff
2021-06-02 Gereon KremerMove public wrapper functions out of options class... tree | commitdiff
2021-05-27 Andrew ReynoldsFix CEGQI for datatypes with Boolean subfields (#6630) tree | commitdiff
2021-05-27 Aina NiemetzFP: Rename FLOATINGPOINT_PLUS to FLOATINGPOINT_ADD... tree | commitdiff
2021-05-26 Andres Noetzli More precise includes of `Node` constants (#6617) tree | commitdiff
2021-05-24 Andrew ReynoldsMove proof utilities to src/proof/ (#6611) tree | commitdiff
2021-05-24 Andrew ReynoldsFix instance of no rewrite in extended rewriter (#6610) tree | commitdiff
2021-05-21 Andrew ReynoldsFix and refactor relevant domain (#6528) tree | commitdiff
2021-05-21 Andrew ReynoldsUpdate to sygus standard output for check-synth respons... tree | commitdiff
2021-05-21 Aina NiemetzBV: Rename BITVECTOR_PLUS to BITVECTOR_ADD. (#6589) tree | commitdiff
2021-05-20 Haniel BarbosaRemove old unsat cores (#6581) tree | commitdiff
2021-05-18 Abdalrhman MohamedLoop over terms to reconstruct instead of obligations... tree | commitdiff
2021-05-13 Mathias PreinerAdd std::hash overloads for Node, TNode and TypeNode... tree | commitdiff
2021-05-07 Andrew ReynoldsSimplifications to expand definitions (#6487) tree | commitdiff
2021-05-06 Andrew ReynoldsDiscard duplicate terms in patterns (#6501) tree | commitdiff
2021-05-05 Andrew ReynoldsDo not have quantifiers model inherit from theory model... tree | commitdiff
2021-04-29 Gereon KremerAvoid exponential explosion of small constant in CEGQI... tree | commitdiff
2021-04-28 Gereon KremerRemove exception headers from options.h (#6456) tree | commitdiff
2021-04-27 Andrew ReynoldsFix refutational soundness bug in quantifier prenexing... tree | commitdiff
2021-04-26 Gereon KremerFirst part of options refactoring (#6428) tree | commitdiff
2021-04-25 Andrew ReynoldsUse fast enumeration by default for Boolean predicate... tree | commitdiff
2021-04-23 Andrew ReynoldsEnable strings exp by default for strings specific... tree | commitdiff
2021-04-21 Mathias PreinerGoodbye CVC4, hello cvc5! (#6371) tree | commitdiff
2021-04-20 Aina NiemetzQuantifiers: Move implementation of type rules to cpp... tree | commitdiff
2021-04-19 Andrew ReynoldsFully incorporate quantifiers macros into ppAssert... tree | commitdiff
2021-04-15 Aina NiemetzRename occurrences of CVC4 to CVC5. (#6351) tree | commitdiff
2021-04-14 Gereon KremerRefactor / reimplement statistics (#6162) tree | commitdiff
next