projects / cvc5.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Minor cleanup of proof messages (#7494)
[cvc5.git] / test /
2021-10-29 Andrew ReynoldsFix model construction for higher order involving irrel... tree | commitdiff
2021-10-29 Andrew ReynoldsAdd PfRule ARITH_POLY_NORM (#7501) tree | commitdiff
2021-10-28 Gereon KremerFix proof for xor in circuit propagator (#7525) tree | commitdiff
2021-10-28 Haniel Barbosa[proofs] Fix assertion in EqProof conversion (#7522) tree | commitdiff
2021-10-28 Andrew V. JonesAdd support for checking if a `-Wno` flag exists before... tree | commitdiff
2021-10-28 Abdalrhman MohamedAdd a `define-fun` command for each `:named` term.... tree | commitdiff
2021-10-28 Abdalrhman MohamedFix `(set-info <sexpr>)` parsing and printing bugs... tree | commitdiff
2021-10-27 Andrew ReynoldsAdd missing API checks to getValue (#7475) tree | commitdiff
2021-10-27 Andres Noetzli[Regression Script] Fix use of undefined variables... tree | commitdiff
2021-10-27 Andres NoetzliRequire ITE branches to be first class types (#7508) tree | commitdiff
2021-10-27 Andrew ReynoldsFix care graph computation for higher-order (#7474) tree | commitdiff
2021-10-27 Andrew ReynoldsFix model unsoundness for relation join (#7511) tree | commitdiff
2021-10-27 Andrew ReynoldsAvoid non-terminating check with assumptions in strings... tree | commitdiff
2021-10-27 Andrew ReynoldsDeterministic variables for RE elim (#7489) tree | commitdiff
2021-10-27 Gereon KremerMake --version exit (#7506) tree | commitdiff
2021-10-26 Haniel Barbosa[proofs] Fix singleton check in MACRO_RES post-processi... tree | commitdiff
2021-10-26 Haniel Barbosa[proofs] Reset local var in SatProofManager since incre... tree | commitdiff
2021-10-26 Andrew ReynoldsDisable automatic symmetry in proofs of theory explanat... tree | commitdiff
2021-10-26 Haniel Barbosa[proofs] Fix and simplify CHAIN_RESOLUTION checker... tree | commitdiff
2021-10-26 Andrew ReynoldsAdd regressions for fixed issues (#7495) tree | commitdiff
2021-10-26 Andrew ReynoldsDisable sygus-inst when incremental (#7485) tree | commitdiff
2021-10-25 Andrew ReynoldsAdd new method for enumerating unsat queries with SyGuS... tree | commitdiff
2021-10-25 Andrew ReynoldsJava and python unit tests for mkCardinalityConstraint... tree | commitdiff
2021-10-25 Andrew ReynoldsFix more missing uses of CDProof::isSame (#7491) tree | commitdiff
2021-10-25 Andrew ReynoldsFix support for global declarations (#7480) tree | commitdiff
2021-10-25 mudathirmahgoubAdd inference for count map (#7264) tree | commitdiff
2021-10-25 Andrew ReynoldsReenable proofs on some regressions (#7483) tree | commitdiff
2021-10-25 Andres Noetzli[Regression Script] Support older Python versions ... tree | commitdiff
2021-10-24 Andrew ReynoldsAdd new eager conflict detection in strings for integer... tree | commitdiff
2021-10-22 Andrew ReynoldsAdd requires libpoly to regression (#7467) tree | commitdiff
2021-10-22 mudathirmahgoubRefactor java package name from cvc5 to io.github.cvc5... tree | commitdiff
2021-10-22 Haniel Barbosa[proof] Fixing CHAIN_RESOLUTION checker (#7465) tree | commitdiff
2021-10-22 Gereon KremerFix out-of-sync pruning in CDCAC proofs (#7470) tree | commitdiff
2021-10-22 Gereon KremerFix another double negation proof issue (#7468) tree | commitdiff
2021-10-22 Andrew ReynoldsAdd more abduction regressions (#7461) tree | commitdiff
2021-10-22 Gereon KremerMake CAD proofs user context dependent (#7466) tree | commitdiff
2021-10-22 yoni206Making `IntBlaster` inherit from `EnvObj` (#7431) tree | commitdiff
2021-10-22 Andrew ReynoldsDo not use global proxy variable attribute for strings... tree | commitdiff
2021-10-22 mudathirmahgoubAdd missing methods to Solver.java (#7299) tree | commitdiff
2021-10-21 Gereon KremerAlso fix case of negated ite (#7454) tree | commitdiff
2021-10-21 Gereon KremerFix symmetric proof issue for ITE in circuit propagator... tree | commitdiff
2021-10-21 Andres Noetzli[Regression Script] Fix printing of error diff (#7451) tree | commitdiff
2021-10-21 Haniel Barbosa[proofs] Fix open proof in SAT solver due to cycles... tree | commitdiff
2021-10-21 Gereon KremerAdd regression (#7447) tree | commitdiff
2021-10-21 Gereon KremerFix incorrect proof from ITE in circuit propagator... tree | commitdiff
2021-10-21 Andres NoetzliRefactor regressions script (#7249) tree | commitdiff
2021-10-21 Andrew ReynoldsMake cardinality constraint a nullary operator (#7333) tree | commitdiff
2021-10-21 Andres NoetzliEnable and fix dump test (#7387) tree | commitdiff
2021-10-21 Gereon KremerFix (#7437) tree | commitdiff
2021-10-20 Andrew ReynoldsEnable some previously failing regressions (#7434) tree | commitdiff
2021-10-20 Aina Niemetzapi: Add Solver::mkSepEmp(). (#7432) tree | commitdiff
2021-10-20 Andrew ReynoldsAdd regressions for fixed issues (#7421) tree | commitdiff
2021-10-20 yoni206Add `isNull` and `isUpdater` to `Sort` class of python... tree | commitdiff
2021-10-20 Andrew ReynoldsCheck for higher-order variables in TheoryUF::ppRewrite... tree | commitdiff
2021-10-20 Andrew ReynoldsMake SyGuS solver robust to non-closed enumerable sorts... tree | commitdiff
2021-10-20 Andrew ReynoldsCheck whether abduct option is enabled (#7418) tree | commitdiff
2021-10-20 Aina Niemetzapi: Rename get(BV|FP)*Size functions for consistency... tree | commitdiff
2021-10-20 Andrew ReynoldsUse codatatype bound variables for codatatype values... tree | commitdiff
2021-10-20 Andrew ReynoldsReimplement support for relational triggers (#7063) tree | commitdiff
2021-10-20 Andrew ReynoldsDo not make assumption about model for Boolean variable... tree | commitdiff
2021-10-20 Andrew ReynoldsCorrectly parse uninterpreted constant values in get... tree | commitdiff
2021-10-19 Andrew ReynoldsFix expected conclusion for EQ_RESOLVE when expanding... tree | commitdiff
2021-10-19 Andrew ReynoldsSupport sequences of fixed finite cardinality (#7371) tree | commitdiff
2021-10-19 Andrew ReynoldsFix issue related to sanity checking integer models... tree | commitdiff
2021-10-18 Andrew ReynoldsAdd regression for fixed issue (#7395) tree | commitdiff
2021-10-18 Abdalrhman MohamedMove check for experimental arrays features to `theory_... tree | commitdiff
2021-10-15 Andrew ReynoldsAdd more regressions for fixed issues (#7382) tree | commitdiff
2021-10-15 Alex OzdemirFix bad cast in the python API (#7359) tree | commitdiff
2021-10-15 Andrew ReynoldsFix issues related to proofs of lemmas with duplicate... tree | commitdiff
2021-10-14 Andrew ReynoldsAdd regressions for fixed issues (#7369) tree | commitdiff
2021-10-14 Gereon KremerImprove ManagedStreams (#7367) tree | commitdiff
2021-10-14 Andrew ReynoldsAdd regression for fixed issue (#7365) tree | commitdiff
2021-10-14 Andrew ReynoldsFix quantifiers variable elimination for parametric... tree | commitdiff
2021-10-11 Aina NiemetzRename SmtScope to SolverEngineScope. (#7284) tree | commitdiff
2021-10-11 Andrew ReynoldsConnect the LFSC printer (#7323) tree | commitdiff
2021-10-07 Andrew ReynoldsMove preprocessor to smt solver (#7321) tree | commitdiff
2021-10-07 Gereon KremerAdd new versioning scheme (#7253) tree | commitdiff
2021-10-07 Andrew ReynoldsMake the cardinality of the alphabet of strings configu... tree | commitdiff
2021-10-07 mudathirmahgoubAdd missing functions in Term.java (#7297) tree | commitdiff
2021-10-07 Gereon KremerChange behaviour of Term::getRealValue() (#7316) tree | commitdiff
2021-10-06 Gereon KremerChange semantics of dumpUnsatCoresFull (#7314) tree | commitdiff
2021-10-05 Gereon KremerFinish refactoring on option handlers (#7295) tree | commitdiff
2021-10-04 Andrew ReynoldsEliminating static calls to rewriter from strings ... tree | commitdiff
2021-10-01 mudathirmahgoubUpdate java examples using the new Java API (#7225) tree | commitdiff
2021-10-01 Andrew ReynoldsFix ascription check for return types on ordinary funct... tree | commitdiff
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-30 Gereon KremerRefactor our static builds (#7251) tree | commitdiff
2021-09-30 mudathirmahgoubFinish the Java Api (#6396) tree | commitdiff
2021-09-30 Andrew ReynoldsSimplify the syntax and representation of the separatio... tree | commitdiff
2021-09-29 Abdalrhman MohamedRemove support for extended `(check-sat <term>)` comman... tree | commitdiff
2021-09-29 Andrew ReynoldsProperly restrict PBE symmetry breaking for abduction... tree | commitdiff
2021-09-29 Andrew ReynoldsUpdate the syntax for tuples in smt2 (#7265) tree | commitdiff
2021-09-29 Gereon Kremerremove stuff (#7258) tree | commitdiff
2021-09-29 mudathirmahgoubAdd Sort.java to the java API (#6382) tree | commitdiff
2021-09-24 Andrew ReynoldsEliminate calls to Rewriter::rewrite from strings entai... tree | commitdiff
2021-09-23 Andrew ReynoldsImplement alpha equivalence proofs (#7066) tree | commitdiff
2021-09-22 Mathias PreinerRemove CVC language support (#7219) tree | commitdiff
2021-09-22 Andrew ReynoldsTowards standard usage of evaluator (#7189) tree | commitdiff
2021-09-22 OuyanchengFix solver_black unit test (#7233) tree | commitdiff
next