Nonlin LA preds

[BritikovKI]

Allows to create nonlin functions

Removed all of the constraints for the creation of nonlin predicates inside of the functions. Only the assertions are checked for nonlinearity

[aehyvari]

The code fails with this input

(set-logic QF_LIA)
(define-fun uninterp_mul ((a Int) (b Int)) Int (mod a b))
(assert (= (uninterp_mul 1 2) 0))
(check-sat)
(exit)

Here's the output:

(error "Divisor must be constant in linear logic")

(error "define-fun returns an unknown sort")

(error "Unknown symbol `uninterp_mul Int Int'")

(error "assertion returns an unknown sort")

sat

[aehyvari]

For our limited form of axioms this might actually be just enough. One thing is missing before I can put this to our production: To be sure that we're running the correct version, I'd need to have the version information from opensmt. See issue #800 .

[BritikovKI]

Ok, I think generally PR is over

Though, we definitely need some sort of error handling, LANonLinearException produces errors with different format under different complilers rn. Should it be a different issue though?

[Tomaqa]

Kostia probably refers to the fact that we do not catch exceptions at the top level of the application (such as in bin/opensmt.cc), which results in UB.

[blishko]

Kostia probably refers to the fact that we do not catch exceptions at the top level of the application (such as in bin/opensmt.cc), which results in UB.

I don't see any mention of undefined behaviour in the link you provided. Unspecified, yes. Undefined, no.

[blishko]

Ok, I think generally PR is over

Though, we definitely need some sort of error handling, LANonLinearException produces errors with different format under different complilers rn. Should it be a different issue though?

I agree that we can catch the exception, probably at the level of a call to solve of MainSolver and return unknown. SMT-LIB has a concept of "reason for unknown", which we should probably implement.

[blishko]

I suggest the following: First, let's fix the terminology. Our arithmetic sums are basically (multivariate) polynomials. Polynomial is composed of terms. This is unfortunately an overloaded word in our domain, so I suggest to refer to it as poly-term. poly-term is a product of a coefficient and zero or more variables (We can restrict our case to variables with degree at most one for now). The coefficient is implicit if it is 1.

With this terminology I suggest to rename the method splitTermToVarAndConst to splitPolyTerm, but it would be doing the same thing: it would return a pair where the first component is the coefficient of the poly-term and the second coefficient is the rest of the poly-term. In case there is more than one variable, this will create a new term, so the method will have to be non-const. I think that should be OK, I hope.

[BritikovKI]

Ok, I unfortunately had to strip out const out of the termSort, but otherwise it should be Ok...

Also to comment on:

poly-term is a product of a coefficient and zero or more variables (We can restrict our case to variables with degree at most one for now). The coefficient is implicit if it is 1.

Poly-term might be also a product of a coefficient and other poly-terms (in case if we have int divisions, and those now might be divisions of variables as well)

[BritikovKI]

New sym_Int_TIMES_NONLIN/sym_Real_TIMES_NONLIN was added and a draft implementation to handle it Introducing new operator for nonlin multiplication might've been not the best choice, I'm not sure now how to separate lin and nonlin multiplication otherwise (bc if they have the same operators then sym_Int_TIMES_NONLIN = sym_Int_TIMES)... Other then that it should be more or less representative of the new approach, it is basically (* const (* var_1 ... var_n))

This is the cvc5 files I got the inspiration from: link

TNode definition: link

NONLINEAR_MULT type is defined here(it is synonym of MULT): link

[aehyvari]

New sym_Int_TIMES_NONLIN/sym_Real_TIMES_NONLIN was added and a draft implementation to handle it Introducing new operator for nonlin multiplication might've been not the best choice, I'm not sure now how to separate lin and nonlin multiplication otherwise (bc if they have the same operators then sym_Int_TIMES_NONLIN = sym_Int_TIMES)

The new symbols make somehow a lot of sense to me at this point. But is it really necessary to use the string representation mul for nonlinear stuff? Couldn't it use the same string *? I'm worried that if we print these out (say, for learned clauses, or models in UF, or something similar) nobody will be able to parse them.

[blishko]

I agree that we should use the same symbol. For that, we need to change SymStore::newSymb to allow it to skip the check if the same symbol already exist, and force it to create a new one.

[BritikovKI]

Ok, it is possible to have just a single symbol but it creates a block of problems:

1. We still want to detect same symbols and reuse same symrefs for them, as an example: 1,-1,0. Because of them we can't just remove the check for same symrefs
2. If we have two '' for INT_MULT and INT_MULT_NONLIN it creates ambiguity for multiplication during lookupSymbol operation, problem here as well that two `are also somewhat synonimous and separation only happens inside as we splitMULT` into linear multiplication and nonlinear multiplication...

My idea would be to introduce some sort of boolean as an additional parameter for a Symbol, which will mark if we should create a duplicate or not. I'm though not sure how to avoid additional check in the PtStore

[BritikovKI]

Maybe we can have some subSymRefs? Basically we will have one SymRef Times, which will have two subSymRefs: TimesLin and TimesNonlin, those will not exist as a separate symbol but will only exist internally, splitting Times into two separate categories

[Tomaqa]

I think that we should go for a more systematic solution. Both multiplication symbols can be clearly distinguished based on their arguments: assuming only binary multiplication, linear mult. must contain a constant. Whether an argument is a constant or a variable should be handled in lookupSymbol - it is not enough to just handle sorts. I do not have a deeper knowledge within this area, so currently I cannot give you a concrete hint, but I guess there must be a way how OpenSMT distinguish variables and constants. Following such attitude, the selection should yield just one candidate symbol, not two.

[BritikovKI]

Whether an argument is a constant or a variable should be handled in lookupSymbol

It would mean that we need to import Logic to PTStore which I don't think is a good idea to be honest, plus in this case it would be even worse because it will also require us to use ArithLogic to check if args is a var or not...

[BritikovKI]

I've introduced notion of "subSymbol", it is basically a SymRef, but it is purely internal as it is not stored in the symbolTable so it won't get parsed