Propagate fresh terms of Relations to the instantiation engine in SatML

[Halbaroth]

While working on #1095, I noticed that the test of the PR #1211, which answers unknown on next, will answer unsat with FunSAT but still answer unknown with SatML. I thought that #1095 will solve this issue but it is trigger a more serious issue in SatML.

Let us recall the context. We try to solve this problem:

(set-logic ALL)
(declare-datatype t ((B (i Int))))

(declare-const e t)

(assert ((_ is B) e))
(assert (forall ((n Int)) (distinct e (B n))))
(check-sat)

In Adt_rel, we process the assertion (_ is B) e and produce a fresh term, says k, such that e = (B k).

• In FunSAT, this new term is added to the instantiation engine and the trigger of the second assertion is (B n). So we produce the substitution n --> k and we assert the predicate e <> (B n). Contradiction!
• In SatML, we never propagate the fresh term k. This issue have been noticed by Mohamed:
  

  alt-ergo/src/lib/reasoners/satml.ml

  Lines 1086 to 1090 in 35c0f14

  	(* XXX what to do with the other results of Th.assume ? *)
  	let t,_,cpt =
  	Th.assume ~ordered:false
  	(List.rev facts) env.unit_tenv
  	in

  
  

  alt-ergo/src/lib/reasoners/satml.ml

  Lines 1160 to 1164 in 35c0f14

  	(* XXX what to do with the other results of Th.assume ? *)
  	let t,_,cpt =
  	Th.assume ~ordered:(not (Options.get_cdcl_tableaux_th ()))
  	(List.rev !facts) env.tenv
  	in

  
  The ignored term is the set of fresh terms created by the relations.

The current design of SatML makes difficult this propagation. Indeed, the SAT solver SatML has been designed as a pure SAT solver. It do not know what is a term and in particular it has no access to the instantiation engine. All this stuff is located in Satml_frontend.

I have no idea how to solve this issue without using hacks. I believe that Satml_frontend should not exist. A SMT solver is not a SAT solver + theory reasoners. You need to interlace a SAT solver and theory reasoners to carry out good performance and trying to separate them makes life harder.

I will write a hack to compare it with FunSAT. It could reduce a bit the difference between them (but I have low expectations because during the last dev meeting, @bclement-ocp told us that most of tests only solved by FunSAT were full of arrays and arrays are not affected by this issue).

[bclement-ocp]

Oh, I forgot this was an issue for theories that create fresh terms… I think for the purpose of #1095 as long as there are no regressions it is OK if we are able to prove with only one of the solvers (although we should duplicate the test, with a note and reference to this issue in both tests).

I have no idea how to solve this issue without using hacks. I believe that Satml_frontend should not exist.

The preparatory work I am doing for SMT-LIB floats should help here as it moves a large chunk of Satml_frontend into Satml (or rather, it inverses the dependency so that Satml calls term-related functions instead of being done from the outside by Satml_frontend), enough that I think we would be able to deal with this properly. I am on other projects at the moment, so I am not sure when it will be done — hopefully sometime next month.

@bclement-ocp told us that most of tests only solved by FunSAT were full of arrays and arrays are not affected by this issue

If I recall correctly the difference on arrays is between CDCL and CDCL-Tableaux, not between CDCL(-Tableaux) and FunSAT. I did not make comparisons with FunSAT recently.