Add the theory part of model generation
And check the model before sat
Showing
- src_colibri2/core/datastructure.ml 6 additions, 6 deletionssrc_colibri2/core/datastructure.ml
- src_colibri2/core/datastructure.mli 10 additions, 3 deletionssrc_colibri2/core/datastructure.mli
- src_colibri2/core/demon.ml 8 additions, 1 deletionsrc_colibri2/core/demon.ml
- src_colibri2/core/demon.mli 1 addition, 0 deletionssrc_colibri2/core/demon.mli
- src_colibri2/core/egraph.ml 14 additions, 1 deletionsrc_colibri2/core/egraph.ml
- src_colibri2/core/events.mli 3 additions, 0 deletionssrc_colibri2/core/events.mli
- src_colibri2/core/ground.ml 45 additions, 4 deletionssrc_colibri2/core/ground.ml
- src_colibri2/core/ground.mli 3 additions, 0 deletionssrc_colibri2/core/ground.mli
- src_colibri2/core/interp.ml 242 additions, 66 deletionssrc_colibri2/core/interp.ml
- src_colibri2/core/interp.mli 10 additions, 0 deletionssrc_colibri2/core/interp.mli
- src_colibri2/popop_lib/popop_stdlib.ml 20 additions, 40 deletionssrc_colibri2/popop_lib/popop_stdlib.ml
- src_colibri2/popop_lib/popop_stdlib.mli 4 additions, 3 deletionssrc_colibri2/popop_lib/popop_stdlib.mli
- src_colibri2/solver/scheduler.ml 73 additions, 38 deletionssrc_colibri2/solver/scheduler.ml
- src_colibri2/stdlib/context.ml 145 additions, 59 deletionssrc_colibri2/stdlib/context.ml
- src_colibri2/stdlib/context.mli 43 additions, 0 deletionssrc_colibri2/stdlib/context.mli
- src_colibri2/stdlib/wto.ml 8 additions, 4 deletionssrc_colibri2/stdlib/wto.ml
- src_colibri2/stdlib/wto.mli 4 additions, 1 deletionsrc_colibri2/stdlib/wto.mli
- src_colibri2/tests/solve/smt_lra/sat/arith_mult_not_linear_in_conflict.smt2 3 additions, 3 deletions.../solve/smt_lra/sat/arith_mult_not_linear_in_conflict.smt2
- src_colibri2/tests/solve/smt_uf/sat/boolexpup.smt2 3 additions, 3 deletionssrc_colibri2/tests/solve/smt_uf/sat/boolexpup.smt2
- src_colibri2/tests/tests_LRA.ml 2 additions, 1 deletionsrc_colibri2/tests/tests_LRA.ml
Loading
Please register or sign in to comment